Nuprl Lemma : adjacent-member
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
x
,
y
:
T
. adjacent(
T
;
L
;
x
;
y
)
{(
x
L
) & (
y
L
)}
latex
ProofTree
Definitions
(
x
l
)
,
x
:
A
B
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
before
y
l
,
{
T
}
,
Type
,
,
x
:
A
B
(
x
)
,
P
&
Q
,
type
List
,
adjacent(
T
;
L
;
x
;
y
)
Lemmas
adjacent
wf
,
l
member
wf
,
guard
wf
,
adjacent-before
,
l
before
member
,
l
before
member2
origin
T:Type, L:(T List), x, y:T. adjacent(T;L;x;y) 
{(x 
L) & (y L)}
T:Type, L:(T List), x, y:T. adjacent(T;L;x;y) {(x L) & (y L)}
l)
B(x) Qx:A. B(x) l
B(x)